/LMAR=0/XLINE=4/FONT#1=BAXL30/FONT#0=BAXI30[  P,JRA]/FONT#2=BAXB30/FONT#3=NGR25/FONT#4=BAXI22/FONT#5=BAXL22/FONT#6=GRK30/FONT#7=SUP/FONT#8=SPEC[  P,JRA]/FONT#9=BDR40/FONT#10=MATH30/FONT#11=METSB/FONT#12=NONMBI/FONT#13=GERM35/FONT#16=NGB30/FONT#15=ZERO30
␈↓ α␈↓␈↓ 
∀␈↓CONTENTS  ␈↓

␈↓"β␈↓ α␈↓	pub is a crock
␈↓ α␈↓␈↓ 	y␈↓CONTENTS  14␈↓

␈↓"β␈↓ α␈↓↓pub is more of a crock
␈↓ α␈↓␈↓ 
␈↓CONTENTS  i␈↓

␈↓"β␈↓ α␈↓↓page it
␈↓ α␈↓␈↓ 
α␈↓CONTENTS  ii␈↓








␈↓"β␈↓ α␈↓	␈↓ βvT A B L E   O F   C O N T E N T S 
␈↓ α␈↓␈↓ λ,␈↓  ␈↓
␈↓ α␈↓␈↓ λ␈↓  1␈↓

␈↓"β␈↓ α␈↓␈↓ ∧9␈↓αRunnable Specification As a Design Tool␈↓↓


␈↓"β␈↓ α␈↓↓␈↓ ¬tRuth E. Davis
␈↓"β␈↓ α␈↓↓␈↓ β\Electrical Engineering and Computer Science Department
␈↓"β␈↓ α␈↓↓␈↓ ¬*University of Santa Clara
␈↓"β␈↓ α␈↓↓␈↓ ¬;Santa Clara, CA 95053






␈↓"β␈↓ α␈↓␈↓↓There are at least four phases in the development of "correct" software.
␈↓"β␈↓ α␈↓↓␈↓ αH1)␈αUnderstanding␈α
the␈αproblem.␈α
 The␈αprogram␈α
designer␈αmay␈α
work␈αwith␈αintended␈α
users
␈↓ α␈↓↓of␈α⊗the␈α⊗system␈α↔to␈α⊗develop␈α⊗an␈α⊗intuitive␈α↔understanding␈α⊗of␈α⊗the␈α⊗problem␈α↔and␈α⊗possible
␈↓ α␈↓↓approaches to its solution.
␈↓"β␈↓ α␈↓↓␈↓ αH2)␈α∀Formal␈α∀specification.␈α∪ Once␈α∀the␈α∀designer␈α∀knows␈α∪intuitively␈α∀how␈α∀to␈α∀solve␈α∪the
␈↓ α␈↓↓problem, the solution must be specified unambiguously.
␈↓"β␈↓ α␈↓↓␈↓ αH3) Programming.  An implementation of the specification is programmed.
␈↓"β␈↓ α␈↓↓␈↓ αH4)␈α
Verification.␈α The␈α
implementation␈αdeveloped␈α
in␈αstep␈α
three␈αis␈α
shown␈αto␈α
satisfy␈αthe
␈↓ α␈↓↓formal specification of step two.
␈↓"β␈↓ α␈↓↓␈↓ αHThere␈α∞is␈α∂a␈α∞certain␈α∂amount␈α∞of␈α∞testing␈α∂and␈α∞debugging␈α∂that␈α∞goes␈α∞on␈α∂at␈α∞each␈α∂of␈α∞these
␈↓ α␈↓↓stages␈α⊃until␈α⊃one␈α⊃is␈α⊃satisfied␈α⊃with␈α⊃the␈α⊂current␈α⊃step␈α⊃and␈α⊃moves␈α⊃on␈α⊃to␈α⊃the␈α⊃next.␈α⊂ Several
␈↓ α␈↓↓verification␈α
techniques␈α
have␈α
been␈α
developed␈α
to␈α
assist␈α
in␈α
accomplishing␈α
step␈α
four.␈α
 However,
␈↓ α␈↓↓even␈αafter␈αa␈αproof␈αis␈α
completed␈αwe␈αcannot␈αclaim␈αto␈α
have␈αa␈α"correct"␈αprogram,␈αonly␈αone␈α
that
␈↓ α␈↓↓satisfies the given specification.
␈↓"β␈↓ α␈↓↓␈↓ αHRather␈α∞than␈α∞write␈α∞a␈α∞program,␈α∞being␈α
guided␈α∞by␈α∞the␈α∞specification,␈α∞and␈α∞then␈α∞prove␈α
it
␈↓ α␈↓↓satisfies␈α
the␈α
specifications,␈α
one␈α
can␈α
automatically␈α
generate␈α
a␈α
program␈α
from␈α
the␈α
specifications
␈↓ α␈↓↓that␈αis␈α
guaranteed␈αto␈α
preserve␈αthe␈α
semantics,␈αthus␈α
obviatiing␈αthe␈α
need␈αfor␈α
the␈αverification
␈↓ α␈↓↓step entirely [1].
␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
truly␈α
creative␈α
(and␈α
most␈α
difficult)␈α
step␈α
in␈α
the␈α
development␈α
of␈α
a␈α
program␈α∞is␈α
the
␈↓ α␈↓↓construction␈α
of␈α
an␈α
acceptable␈α
formal␈α∞specification␈α
from␈α
an␈α
intuitive␈α
understanding␈α∞of␈α
the
␈↓ α␈↓↓problem.␈α
 Thus,␈αour␈α
efforts␈α
should␈αbe␈α
placed␈α
on␈αdeveloping␈α
design␈α
tools␈αto␈α
help␈α
with␈αthe
␈↓ α␈↓↓construction and testing of the specification.
␈↓"β␈↓ α␈↓↓␈↓ αHHow␈α∂does␈α∂one␈α∂"debug"␈α∂a␈α∂specification?␈α∂ We␈α∂cannot␈α∂hope␈α∂to␈α∂formally␈α∂prove␈α∂that␈α∂a
␈↓ α␈↓↓specification␈α
is␈α
"correct"␈α
with␈α
respect␈α
to␈α
our␈α
intuition,␈αbut␈α
we␈α
can␈α
at␈α
least␈α
test␈α
it␈α
to␈α
see␈αthat␈α
it
␈↓ α␈↓↓conforms to our intuition in specific cases.
␈↓"β␈↓ α␈↓↓␈↓ αHGuttag␈αand␈αHorning␈α[2]␈αpresent␈αan␈αalgebraic␈αspecification␈αtechnique␈αas␈αa␈αdesign␈αtool.
␈↓ α␈↓↓As␈αan␈α
example␈αthey␈α
describe␈αpart␈α
of␈αthe␈α
specification␈αof␈α
a␈αhigh-level␈α
interface␈αto␈αa␈α
flexible
␈↓ α␈↓↓display␈αand␈αdiscuss␈αthe␈αanalysis␈αof␈αthe␈αspecification.␈α A␈αsalient␈αfeature␈αof␈αtheir␈αapproach␈αis
␈↓ α␈↓↓the␈αability␈αto␈α"ask␈αquestions"␈αof␈αthe␈αspecification,␈αderive␈αanswers,␈αand␈αchange␈αthe␈αdesign␈αif
␈↓ α␈↓↓the answers are unacceptable.  In this way they hope to test and debug the specification.
␈↓"β␈↓ α␈↓↓␈↓ αHI␈α∂suggest␈α∂that␈α⊂Horn␈α∂clauses␈α∂provide␈α∂a␈α⊂much␈α∂better␈α∂specification␈α∂language␈α⊂than␈α∂do
␈↓ α␈↓↓algebraic␈α
axioms.␈α The␈α
two␈αlanguages␈α
are␈α
closely␈αrelated;␈α
it␈αis␈α
a␈αsimple␈α
matter␈α
to␈αtranslate
␈↓ α␈↓↓between␈α∂them.␈α∂ The␈α∂ease␈α⊂of␈α∂writing␈α∂a␈α∂specification␈α∂in␈α⊂one␈α∂language␈α∂versus␈α∂the␈α⊂other␈α∂is
␈↓ α␈↓↓undoubtedly␈α
a␈αmatter␈α
of␈αpersonal␈α
taste␈αand␈α
depends␈α
largely␈αon␈α
which␈αlanguage␈α
one␈αis␈α
more
␈↓ α␈↓␈↓ β␈↓  2␈↓

␈↓"β␈↓ α␈↓↓familiar␈α
with.␈α
 The␈α
same␈α
may␈α
be␈α
said␈αof␈α
the␈α
readability␈α
of␈α
a␈α
specification.␈α
 Horn␈αclauses,␈α
as
␈↓ α␈↓↓well␈α
as␈α∞algebraic␈α
axioms,␈α
can␈α∞be␈α
analyzed␈α∞for␈α
answers␈α
to␈α∞specific␈α
questions␈α∞and␈α
modified
␈↓ α␈↓↓accordingly.
␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
major␈α
distinction␈α
between␈α
the␈α
two␈α
methods␈α
is␈α
the␈α
manner␈α
in␈α
which␈αquestions␈α
can
␈↓ α␈↓↓be␈α∩handled.␈α∩ With␈α∩the␈α∩Guttag-Horning␈α∩approach,␈α∩an␈α∩informal␈α∩question␈α∩is␈α∩posed␈α⊃and
␈↓ α␈↓↓submitted␈α∃to␈α⊗an␈α∃"expert"␈α⊗who␈α∃reformulates␈α⊗the␈α∃question,␈α⊗often␈α∃generalizing␈α⊗it.␈α∃The
␈↓ α␈↓↓questioner␈αmust␈αthen␈αbe␈αconvinced␈αthat␈αthe␈αformal␈αstatement␈αdeveloped␈αby␈αthe␈αexpert␈αdoes
␈↓ α␈↓↓indeed␈αreflect␈αthe␈αoriginal␈αquestion,␈αand␈αan␈αanswer␈αto␈αthe␈αformal␈αquestion␈αwill␈αprovide␈αan
␈↓ α␈↓↓answer␈α⊂to␈α⊃the␈α⊂informal␈α⊃one.␈α⊂ Then␈α⊃an␈α⊂attempt␈α⊃is␈α⊂made␈α⊃to␈α⊂derive␈α⊃an␈α⊂answer␈α⊃from␈α⊂the
␈↓ α␈↓↓axioms.
␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
same␈α
approach␈α
may␈α
be␈α
taken␈α
with␈α
Horn␈α
clauses,␈α
but␈α
it␈α
is␈α
not␈α
necessary.␈α
 Since
␈↓ α␈↓↓Horn␈αclauses␈αare␈αexecutable,␈αif␈αthe␈αquestioner␈αwants␈αto␈αknow␈αwhat␈αhappens␈αin␈αa␈αparticular
␈↓ α␈↓↓case,␈αit␈αis␈αpossible␈αto␈αsimply␈α"try␈αit␈αand␈αsee".␈αThe␈αexpert␈αwill␈αstill␈αbe␈αneeded␈αto␈αdevelop␈αthe
␈↓ α␈↓↓specification␈α
and␈α∞to␈α
determine␈α∞what␈α
modifications␈α
should␈α∞be␈α
made␈α∞to␈α
the␈α∞specification␈α
to
␈↓ α␈↓↓change␈αan␈αunacceptable␈αanswer,␈αbut␈αthe␈α"what␈αhappens␈αif␈α...?"␈αquestions␈αno␈αlonger␈αneed␈αbe
␈↓ α␈↓↓formalized.␈α For␈αexample,␈αgiven␈αthe␈αspecification␈αdetailed␈αin␈αthe␈αappendix,␈αand␈αdefinitions
␈↓ α␈↓↓for␈α∀the␈α∃primitives␈α∀(machine␈α∀dependent)␈α∃that␈α∀interface␈α∀the␈α∃underlying␈α∀logic␈α∃with␈α∀the
␈↓ α␈↓↓commands␈αcontrolling␈αthe␈αappearance␈αof␈αthe␈αscreen,␈αit␈αis␈αpossible␈αto␈αexecute␈αlogic␈αprograms
␈↓ α␈↓↓that␈αmanipulate␈αthe␈αdisplay.␈α Ideally,␈αa␈α"front-end"␈αcommand␈αlanguage␈αshould␈αbe␈α
provided
␈↓ α␈↓↓by␈α∂the␈α∂designer(s)␈α⊂that␈α∂enables␈α∂users/testers␈α⊂of␈α∂the␈α∂design␈α∂to␈α⊂make␈α∂their␈α∂requests␈α⊂of␈α∂the
␈↓ α␈↓↓system without having to write them as Horn clauses.
␈↓"β␈↓ α␈↓↓␈↓ αHOnce␈αone␈αis␈αsatisfied␈αthat␈αa␈αHorn␈αclause␈αspecification␈αis␈αa␈αreasonable␈αembodiment␈αof
␈↓ α␈↓↓one's␈αintuition,␈αthe␈αtask␈αof␈αrefining␈αthe␈αspecification␈αinto␈αan␈αefficient␈αprogram␈αcan␈αproceed.
␈↓ α␈↓↓The␈α∞ability␈α∂to␈α∞run␈α∂a␈α∞specification␈α∂makes␈α∞the␈α∞problem␈α∂of␈α∞testing␈α∂and␈α∞debugging␈α∂it␈α∞much
␈↓ α␈↓↓more tractable.
␈↓"β␈↓ α␈↓↓␈↓ αHAs␈αan␈αexample,␈αI␈α
have␈αwritten␈αthe␈αHorn␈α
clause␈αspecification␈αof␈αthe␈α
display␈αspecified
␈↓ α␈↓↓with␈α∂algebraic␈α∂axioms␈α∂by␈α∂Guttag␈α∂and␈α∂Horning.␈α∂ The␈α∂fundamental␈α∂assumption␈α∂is␈α⊂that␈α∂a
␈↓ α␈↓↓user␈αwill␈αwant␈αto␈αbe␈αable␈αto␈αdisplay␈αseveral␈αdistinct␈αblocks␈αof␈αinformation␈αon␈αthe␈αscreen␈αat
␈↓ α␈↓↓once.␈α
 The␈α
top␈αlevel␈α
concept␈α
is␈α
that␈αof␈α
a␈α
␈↓view␈↓↓.␈αA␈α
␈↓view␈↓↓␈α
is␈α
a␈αspatial␈α
arrangement␈α
of␈α␈↓pictures␈↓↓;␈α
a
␈↓ α␈↓↓␈↓picture␈↓↓␈αis␈αa␈αblock␈αof␈αdisplayable␈αinformation.␈αA␈αpicture␈αconsists␈αof␈αa␈αboundary,␈αa␈αcontents,
␈↓ α␈↓↓and␈α
a␈α
coordinate␈α
transformation␈αto␈α
be␈α
applied␈α
in␈αviewing␈α
its␈α
contents.␈α
Examples␈αof␈α
pictures
␈↓ α␈↓↓are␈αthe␈αentire␈αdisplay␈α(with␈αimplicit␈αboundary),␈α
and␈αthe␈αinterior␈αof␈αa␈αfixed␈αrectangle␈αon␈α
the
␈↓ α␈↓↓display; examples of contents are text, figures, and views.
␈↓"β␈↓ α␈↓↓␈↓ αHThe Guttag-Horning specification of picture is as follows:
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓Operators:
␈↓"β␈↓ α␈↓␈↓ αHMakePicture: Contents ␈↓βX␈↓ [Coordinate → TruthValues] ␈↓βX␈↓ [Coordinate → Coordinate]
␈↓"β␈↓ α␈↓␈↓ αH                                 → Picture
␈↓"β␈↓ α␈↓␈↓ αHPicture.Appearance: Picture ␈↓βX␈↓ Coordinate → Illumination
␈↓"β␈↓ α␈↓␈↓ αHPicture.In: Picture ␈↓βX␈↓ Coordinate → TruthValues
␈↓"β␈↓ α␈↓␈↓ αHAxioms:
␈↓"β␈↓ α␈↓␈↓ αHPicture.Appearance(MakePicture(cont, bound, trans), coord)
␈↓"β␈↓ α␈↓␈↓ αH                                        = Contents.Appearance(cont, trans(coord))
␈↓"β␈↓ α␈↓␈↓ αHPicture.In(MakePicture(cont, bound, trans), coord) = bound(coord)
␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α⊂operators␈α∂are␈α⊂listed␈α∂first,␈α⊂giving␈α∂their␈α⊂functionality,␈α∂then␈α⊂the␈α⊂axioms␈α∂defining
␈↓ α␈↓↓them␈α⊃are␈α⊃given.␈α⊂ ␈↓MakePicture␈↓↓␈α⊃is␈α⊃not␈α⊂defined␈α⊃further␈α⊃since␈α⊂it␈α⊃is␈α⊃simply␈α⊃the␈α⊂constructor
␈↓ α␈↓↓function␈α∂for␈α⊂the␈α∂type␈α⊂␈↓Picture␈↓↓.␈α∂ The␈α∂first␈α⊂axiom␈α∂tells␈α⊂us␈α∂that␈α∂the␈α⊂appearance␈α∂at␈α⊂a␈α∂given
␈↓ α␈↓↓coordinate␈α⊂in␈α⊂a␈α⊂␈↓picture␈↓↓␈α⊂is␈α⊂determined␈α⊂by␈α⊂the␈α⊂appearance␈α⊂at␈α⊂a␈α⊂coordinate␈α⊂(the␈α⊃result␈α⊂of
␈↓ α␈↓␈↓ α␈↓  3␈↓

␈↓"β␈↓ α␈↓↓applying␈αthe␈αtransformation␈αto␈αthe␈αoriginal␈αcoordinate)␈αin␈αthe␈α␈↓contents␈↓↓␈αof␈αthe␈α␈↓picture␈↓↓.␈α The
␈↓ α␈↓↓second␈αaxiom␈αindicates␈αthat␈αa␈αcoordinate␈αis␈αin␈αa␈α␈↓picture␈↓↓␈αif␈αit␈αis␈αwithin␈αthe␈αboundary␈αof␈αthe
␈↓ α␈↓↓␈↓picture␈↓↓ as defined by the function ␈↓bound␈↓↓.
␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
specification␈αof␈α
type␈α␈↓Picture␈↓↓␈α
using␈αHorn␈α
clauses␈αis␈α
given␈αbelow.␈α
The␈αHorn␈α
clause
␈↓ α␈↓↓specification␈α↔clearly␈α↔indicates␈α↔the␈α_distinction␈α↔between␈α↔constructor␈α↔functions,␈α_such␈α↔as
␈↓ α␈↓↓␈↓make-picture␈↓↓,␈αand␈αthe␈αpredicates␈αindicating␈αrelationships␈αamong␈αtheir␈αarguments.␈αThe␈αtype
␈↓ α␈↓↓constraints,␈α∪indicating␈α∪functionality␈α∩of␈α∪the␈α∪predicates,␈α∪are␈α∩given␈α∪only␈α∪for␈α∪the␈α∩clause(s)
␈↓ α␈↓↓defining␈αthe␈αtype␈αbeing␈α
specified.␈α Type-checking␈αcan␈αbe␈α
included␈αexplicitly␈αin␈αeach␈α
clause,
␈↓ α␈↓↓however,␈αwe␈α
assume␈αthe␈αrequired␈α
type␈αis␈α
made␈αobvious␈αby␈α
consistent␈αnaming␈α
of␈αvariables
␈↓ α␈↓↓and choose to leave it out of the rest of the specification for the sake of readability.
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓Picture(make-picture(cont, bound, trans)) ← Contents(cont), Boundary(bound),
␈↓"β␈↓ α␈↓␈↓ αH                                                Translation(trans)
␈↓"β␈↓ α␈↓␈↓ αHPicture-Appearance(make-picture(cont, bound, trans), coord, illum) ←
␈↓"β␈↓ α␈↓␈↓ αH        Compute-position(coord,trans,coord'), Contents-appearance(cont, coord'),
␈↓"β␈↓ α␈↓␈↓ αHPicture-In(make-picture(cont, bound, trans), coord, tv) ← Lies-in(coord, bound, tv)
␈↓"β␈↓ α␈↓↓␈↓ αHIn␈α∀the␈α∃Guttag-Horning␈α∀axiomatic␈α∀specification␈α∃of␈α∀the␈α∀display,␈α∃a␈α∀␈↓boundary␈↓↓␈α∃is␈α∀a
␈↓ α␈↓↓function␈αfrom␈α
␈↓Coordinate␈↓↓␈αto␈α␈↓TruthValues␈↓↓␈α
and␈αa␈α
␈↓translation␈↓↓␈αis␈αa␈α
function␈αfrom␈α␈↓Coordinate␈↓↓␈α
to
␈↓ α␈↓↓␈↓Coordinate␈↓↓.␈α∞ Horn␈α∂clause␈α∞syntax␈α∂does␈α∞not␈α∞allow␈α∂functions␈α∞as␈α∂arguments,␈α∞thus␈α∂I've␈α∞treated
␈↓ α␈↓↓␈↓trans␈↓↓␈α↔and␈α⊗␈↓bound␈↓↓␈α↔as␈α⊗objects,␈α↔␈↓Compute-position␈↓↓␈α⊗is␈α↔a␈α⊗predicate␈α↔that␈α↔accomplishes␈α⊗the
␈↓ α␈↓↓translation␈α_from␈α_␈↓coord␈↓↓␈α_to␈α→␈↓coord'␈↓↓␈α_indicated␈α_by␈α_the␈α_Guttag-Horning␈α→␈↓trans␈↓↓,␈α_similarly,
␈↓ α␈↓↓␈↓Lies-in(coord,␈α~bound,␈α→tv)␈↓↓␈α~results␈α→in␈α~␈↓tv␈↓↓␈α→being␈α~bound␈α→to␈α~␈↓true␈↓↓␈α→if␈α~and␈α→only␈α~if␈α→the
␈↓ α␈↓↓Guttag-Horning␈α↔␈↓bound(coord)␈↓↓␈α↔is␈α⊗␈↓true␈↓↓,␈α↔and␈α↔to␈α↔␈↓false␈↓↓␈α⊗if␈α↔and␈α↔only␈α↔if␈α⊗Guttag-Horning
␈↓ α␈↓↓␈↓bound(coord)␈↓↓␈α∞is␈α∞␈↓false␈↓↓.␈α∞ I␈α
would␈α∞not␈α∞need␈α∞the␈α
predicates␈α∞␈↓Compute-position␈↓↓␈α∞and␈α∞␈↓Lies-in␈↓↓␈α∞if␈α
I
␈↓ α␈↓↓had␈α
an␈α∞evaluation␈α
predicate␈α∞which␈α
accepts␈α∞a␈α
function␈α∞and␈α
its␈α∞arguments␈α
and␈α∞applies␈α
the
␈↓ α␈↓↓function␈α∂to␈α∂the␈α∂arguments,␈α∂such␈α∂as␈α∂the␈α∞LISP␈α∂"apply".␈α∂ I␈α∂have␈α∂decided␈α∂to␈α∂remain␈α∞within
␈↓ α␈↓↓first-order␈α∃logic␈α∃and␈α∃the␈α∃strict␈α∃limitations␈α∃of␈α∃Horn␈α∃clauses.␈α∃ Others␈α∃have␈α∀concerned
␈↓ α␈↓↓themselves␈α∂with␈α∂the␈α∞problem␈α∂of␈α∂moving␈α∞to␈α∂second-order,␈α∂as␈α∞shown␈α∂in␈α∂the␈α∞"demonstrate"
␈↓ α␈↓↓predicate used by Ken Bowen and Alan Robinson.
␈↓"β␈↓ α␈↓↓␈↓ αHThe specification of type ␈↓View␈↓↓, given algebraically, is as follows:
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓Operators:
␈↓"β␈↓ α␈↓␈↓ αHView.Empty: → View
␈↓"β␈↓ α␈↓␈↓ αHAddPicture: View ␈↓βX␈↓ Coordinate ␈↓βX␈↓ PictureId ␈↓βX␈↓ Picture → View
␈↓"β␈↓ α␈↓␈↓ αHView.Appearance: View ␈↓βX␈↓ Coordinate → Illumination
␈↓"β␈↓ α␈↓␈↓ αHView.In: View ␈↓βX␈↓ Coordinate → TruthValues
␈↓"β␈↓ α␈↓␈↓ αHFindPictures: View ␈↓βX␈↓ Coordinate → IdList
␈↓"β␈↓ α␈↓␈↓ αHDeletePicture: View ␈↓βX␈↓ PictureId → View
␈↓"β␈↓ α␈↓␈↓ αHAxioms:
␈↓"β␈↓ α␈↓␈↓ αHView.Appearance(AddPicture(v, coord', id, p), coord) =
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓if␈↓ Picture.In(p, Minus(coord, coord'))
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓then␈↓ Picture.Appearance(p, Minus(coord, coord'))
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓else␈↓ View.Appearance(v, coord)
␈↓"β␈↓ α␈↓␈↓ αHView.Appearance(View.Empty, coord)␈↓↓ intentionally left unspecified
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓View.In(View.Empty, coord) = False
␈↓"β␈↓ α␈↓␈↓ αHView.In(AddPicture(v, coord', id, p), coord) =
␈↓"β␈↓ α␈↓␈↓ αH                        Picture.In(p, Minus(coord, coord')) ∨ View.In(v, coord)
␈↓"β␈↓ α␈↓␈↓ αHFindPictures(View.Empty, coord) = IdList.Empty
␈↓"β␈↓ α␈↓␈↓ αHFindPictures(AddPicture(v, coord', id, p), coord) =
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓if␈↓ Picture.In(p, Minus(coord, coord'))
␈↓ α␈↓␈↓ ¬␈↓  4␈↓

␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓then␈↓ IdList.Insert(id, FindPictures(v, coord))
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓else␈↓ FindPictures(v, coord)
␈↓"β␈↓ α␈↓␈↓ αHDeletePicture(View.Empty, id) = View.Empty
␈↓"β␈↓ α␈↓␈↓ αHDeletePicture( AddPicture(v, coord, id', p), id) =
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓if␈↓ PictureId.Equal(id, id')
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓then␈↓ v
␈↓"β␈↓ α␈↓␈↓ αH                ␈↓↓else␈↓ AddPicture(DeletePicture(v, id), coord, id', p)
␈↓"β␈↓ α␈↓↓␈↓ αHGuttag␈αand␈αHorning␈αuse␈αthe␈αconvention␈αof␈αprefixing␈αa␈αfunction␈αname␈αby␈αthe␈αtype␈αit
␈↓ α␈↓↓is␈α
operating␈αon␈α
and␈αa␈α
dot.␈α In␈α
this␈αway␈α
they␈αcan␈α
use␈αthe␈α
same␈αname␈α
for␈α
similar␈αfunctions
␈↓ α␈↓↓being␈αdefined␈αover␈α
several␈αdifferent␈αtypes.␈α
 They␈αchose␈αto␈α
use␈αa␈α0-ary␈αfunction␈α
␈↓View.Empty␈↓↓
␈↓ α␈↓↓to␈α∩indicate␈α∩the␈α∩empty␈α∩view,␈α∩we␈α⊃use␈α∩a␈α∩constant␈α∩␈↓mt-view␈↓↓.␈α∩␈↓AddPicture␈↓↓␈α∩is␈α∩the␈α⊃constructor
␈↓ α␈↓↓function␈α∞for␈α∞type␈α
␈↓View␈↓↓.␈α∞ ␈↓Appearance␈↓↓␈α∞and␈α
␈↓In␈↓↓␈α∞are␈α∞determined␈α
by␈α∞the␈α∞components␈α
(pictures)
␈↓ α␈↓↓making␈α⊂up␈α∂a␈α⊂view.␈α⊂ ␈↓FindPictures␈↓↓␈α∂is␈α⊂a␈α∂function␈α⊂that␈α⊂constructs␈α∂a␈α⊂list␈α∂of␈α⊂␈↓id␈↓↓'s␈α⊂of␈α∂pictures
␈↓ α␈↓↓containing␈α
a␈α
given␈α
coordinate.␈α∞ ␈↓DeletePicture␈↓↓␈α
deletes␈α
a␈α
picture,␈α∞specified␈α
by␈α
its␈α
␈↓id␈↓↓,␈α∞from␈α
a
␈↓ α␈↓↓view.
␈↓"β␈↓ α␈↓↓␈↓ αHAgain,␈α↔using␈α_Horn␈α↔clauses,␈α_we␈α↔indicate␈α↔the␈α_types␈α↔of␈α_arguments␈α↔only␈α_in␈α↔the
␈↓ α␈↓↓specification␈α⊃of␈α⊃␈↓View␈↓↓,␈α⊃and␈α∩assume␈α⊃the␈α⊃desired␈α⊃types␈α∩are␈α⊃made␈α⊃apparent␈α⊃by␈α∩naming␈α⊃of
␈↓ α␈↓↓variables.
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓View(mt-view) ←
␈↓"β␈↓ α␈↓␈↓ αHView(addpicture(v, c, id, p)) ← View(v), Coordinate(c), PictureId(id), Picture(p)
␈↓"β␈↓ α␈↓␈↓ αHView-Appearance(mt-view, coord, x) ←
␈↓"β␈↓ α␈↓␈↓ αH␈↓↓As in the algebraic specification, we leave unspecified the appearance of the
␈↓"β␈↓ α␈↓↓␈↓ αHmt-view at any coordinate.  Since we have no if-then-else, the axiom describing
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓View.Appearance␈↓↓ corresponds to two Horn clauses, one for each alternative.␈↓
␈↓"β␈↓ α␈↓␈↓ αHView-Appearance(addpicture(v, coord', id, p), coord, illum) ←
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-In(p, minus(coord, coord'), true),
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-Appearance(p, minus(coord, coord'), illum)
␈↓"β␈↓ α␈↓␈↓ αHView-Appearance(addpicture(v, coord', id, p), coord, illum) ←
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-In(p, minus(coord, coord'), false),
␈↓"β␈↓ α␈↓␈↓ αH                                View-Appearance(v, coord, illum)
␈↓"β␈↓ α␈↓␈↓ αHView-In(mt-view, coord, false) ←
␈↓"β␈↓ α␈↓␈↓ αH␈↓↓Horn clauses are not allowed alternative conditions. Thus the second axiom for
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓View.In␈↓↓ is handled by the following three Horn clauses, one for each alternative
␈↓"β␈↓ α␈↓↓␈↓ αHmaking the conclusion ␈↓true␈↓↓, and a third to enable us to derive the fact that a
␈↓"β␈↓ α␈↓↓␈↓ αHcoordinate is not in a ␈↓view␈↓↓.
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓View-In(addpicture(v, coord', id, p), coord, true) ←
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-In(p, minus(coord, coord'), true)
␈↓"β␈↓ α␈↓␈↓ αHView-In(addpicture(v, coord', id, p), coord, true) ← View-In(v, coord, true)
␈↓"β␈↓ α␈↓␈↓ αHView-In(addpicture(v, coord', id, p), coord, false) ←
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-In(p, minus(coord, coord'), false),
␈↓"β␈↓ α␈↓␈↓ αH                                View-In(v, coord, false)
␈↓"β␈↓ α␈↓␈↓ αHFindPictures(mt-view, coord, mt-idlist) ←
␈↓"β␈↓ α␈↓␈↓ αHFindPictures(addpicture(v, coord', id, p), coord, idlist-insert(id,idl)) ←
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-In(p, minus(coord, coord'), true),
␈↓"β␈↓ α␈↓␈↓ αH                                FindPictures(v, coord, idl)
␈↓"β␈↓ α␈↓␈↓ αHFindPictures(addpicture(v, coord', id, p), coord, idl) ←
␈↓"β␈↓ α␈↓␈↓ αH                                Picture-In(p, minus(coord, coord'), false),
␈↓"β␈↓ α␈↓␈↓ αH                                FindPictures(v, coord, idl)
␈↓"β␈↓ α␈↓␈↓ αHDeletePicture(mt-view, id, mt-view) ←
␈↓ α␈↓␈↓ β␈↓  5␈↓

␈↓"β␈↓ α␈↓␈↓ αHDeletePicture(addpicture(v, coord, id, p), id, v) ←
␈↓"β␈↓ α␈↓␈↓ αHDeletePicture(addpicture(v, coord, id', p), id, addpicture(v', coord, id', p)) ←
␈↓"β␈↓ α␈↓␈↓ αH                                PictureId-equal(id, id', false),
␈↓"β␈↓ α␈↓␈↓ αH                                DeletePicture(v, id, v')
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓FindPictures␈↓↓␈α∂and␈α∂␈↓DeletePicture␈↓↓␈α∂present␈α∂no␈α∞surprises.␈α∂ Again,␈α∂an␈α∂if-then-else␈α∂in␈α∞an
␈↓ α␈↓↓axiom␈α⊂results␈α∂in␈α⊂two␈α⊂clauses␈α∂in␈α⊂the␈α∂Horn␈α⊂clause␈α⊂specification.␈α∂ A␈α⊂complete␈α⊂Horn␈α∂clause
␈↓ α␈↓↓specification of the display is given in the appendix.
␈↓"β␈↓ α␈↓↓␈↓ αHIn␈α
analyzing␈α
the␈α
specification␈α
using␈α
the␈αalgebraic␈α
axioms␈α
one␈α
needs␈α
an␈α
expert␈α
to␈αgo
␈↓ α␈↓↓between␈α
the␈αquestioner␈α
and␈α
the␈αspecification.␈α
 For␈α
example,␈αand␈α
informal␈α
question␈αasked␈α
of
␈↓ α␈↓↓Guttag␈α∀and␈α∀Horning␈α∀was:␈α∀"Is␈α∀it␈α∀the␈α∀case␈α∀that␈α∀pictures␈α∀are␈α∀not␈α∀transparent␈α∀or␈α∪even
␈↓ α␈↓↓translucent?␈α
I.e.,␈α
if␈α
two␈α
pictures␈α
overlap,␈α
does␈αthe␈α
bottom␈α
one␈α
have␈α
no␈α
effect␈α
on␈α
what␈αone
␈↓ α␈↓↓sees through the top one?". The question was formalized as:
␈↓"β␈↓ α␈↓↓␈↓ αH"Is it true that
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓(∀c,c',w,id,v1,v2)[Picture.In(w,Minus(c,c')) →
␈↓"β␈↓ α␈↓␈↓ αH        [View.Appearance(AddPicture(v1,c',id,w),c)
␈↓"β␈↓ α␈↓␈↓ αH                        = View.Appearance(AddPicture(v2,c',id,w),c)]] ␈↓↓?"
␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α∪formal␈α∪question␈α∪is␈α∪answered␈α∪affirmatively,␈α∪following␈α∪directly␈α∪from␈α∪the␈α∪first
␈↓ α␈↓↓alternative in the first axiom of type ␈↓View␈↓↓.
␈↓"β␈↓ α␈↓↓␈↓ αHIf␈α⊃we␈α⊃so␈α⊃desired,␈α⊃we␈α⊃could␈α⊃formalize␈α⊃the␈α⊃question␈α⊃to␈α⊃be␈α⊃put␈α⊃to␈α⊃our␈α⊃Horn␈α⊃clause
␈↓ α␈↓↓specification␈α⊂and␈α⊃derive␈α⊂the␈α⊂same␈α⊃answer,␈α⊂using␈α⊃the␈α⊂second␈α⊂clause␈α⊃in␈α⊂the␈α⊃definition␈α⊂of
␈↓ α␈↓↓␈↓View-Appearance␈↓↓,␈αbut␈αthere␈α
is␈αno␈αneed.␈α Since␈α
we␈αcan␈αrun␈α
the␈αHorn␈αclause␈αspecification,␈α
all
␈↓ α␈↓↓the␈αuser␈αneed␈αdo␈αis␈αconstruct␈αoverlapping␈αpictures␈αand␈αlook␈αat␈αthe␈αresult.␈αThis␈αis␈αsufficient
␈↓ α␈↓↓to␈αanswer␈αquestions␈αabout␈αspecific␈αcases.␈α If␈αone␈αis␈αinterested␈αin␈αproving␈αgeneral␈αproperties,
␈↓ α␈↓↓then␈α∂we␈α∂must␈α∂fall␈α∂back␈α∂to␈α∂a␈α∂formalization␈α∂of␈α∂the␈α∂question␈α∂and␈α∂formal␈α∂derivation␈α∂of␈α∞an
␈↓ α␈↓↓answer from the specification.
␈↓"β␈↓ α␈↓↓␈↓ αHUsing␈α∩Horn␈α∪clauses␈α∩as␈α∩a␈α∪design␈α∩tool␈α∩we␈α∪enjoy␈α∩all␈α∩the␈α∪benefits␈α∩of␈α∪the␈α∩algebraic
␈↓ α␈↓↓approach,␈α
and␈α
gain␈α
the␈αadvantage␈α
that␈α
testing␈α
is␈αmore␈α
easily␈α
accomplished.␈α
 An␈αexpert␈α
may
␈↓ α␈↓↓still␈α
be␈α
required␈αto␈α
develop␈α
the␈αdesign␈α
specification␈α
and␈αto␈α
modify␈α
it␈αif␈α
necessary,␈α
but␈αthe
␈↓ α␈↓↓analysis␈α∞of␈α∞the␈α∞design␈α
can␈α∞be␈α∞carried␈α∞out␈α
by␈α∞people␈α∞who␈α∞may␈α
be␈α∞experts␈α∞in␈α∞the␈α
problem
␈↓ α␈↓↓domain but not in the specification language.
␈↓"β␈↓ α␈↓↓␈↓ ε	␈↓αReferences␈↓↓
␈↓"β␈↓ α␈↓↓␈↓ αH[1] Davis, R. E., "Generation of Correct Programs from Logic Specifications",
␈↓"β␈↓ α␈↓↓Ph.D. Thesis, Board of Information Sciences, University of California, Santa Cruz, 1979.
␈↓"β␈↓ α␈↓↓␈↓ αH[2]␈αGuttag,␈αJ.,␈αand␈αJ.␈αHorning,␈α"Formal␈αSpecification␈αAs␈αa␈αDesign␈αTool",␈αProceedings
␈↓ α␈↓↓of the ACM Symposium on Principles of Programming Languages, 1980.
␈↓"β␈↓ α␈↓↓␈↓ αH[3] Kowalski, R., ␈↓Logic for Problem Solving, Elsevier North Holland, Inc., 1979.
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧TYPE Picture
␈↓"β␈↓ α␈↓↓␈↓ αHPicture(make-picture(cont,␈α bound,␈α trans))␈α ←␈α!Contents(cont),␈α Boundary(bound),
␈↓ α␈↓↓Translation(trans)
␈↓"β␈↓ α␈↓↓␈↓ αHPicture-Appearance(make-picture(cont,␈α6bound,␈α6trans),␈α6coord,␈α6illum)␈α5←
␈↓ α␈↓↓Compute-position(coord,trans,coord'),␈α≤Contents-appearance(cont,␈α≤coord'),␈α≤Contents(cont),
␈↓ α␈↓↓Boundary(bound),␈α?␈α
Translation(trans),␈α?␈α∞Coordinate(coord),␈α?␈α
Coordinate(coord'),
␈↓ α␈↓↓Illumination(illum)␈αPicture-In(make-picture(cont,␈αbound,␈α
trans),␈αcoord,␈αtv)␈α
←␈αLies-in(coord,
␈↓ α␈↓↓bound,␈α∨tv),␈α∨Contents(cont),␈α∨Boundary(bound),␈α∨Translation(trans),␈α≡Coordinate(coord),
␈↓ α␈↓↓Truth-value(tv)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Picture
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Contents
␈↓"β␈↓ α␈↓↓␈↓ αHContents(mt-contents) ←
␈↓ α␈↓␈↓ β␈↓  6␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHContents(add-component(cont,␈α⊗comp,␈α↔coord))␈α⊗←␈α↔Contents(cont),␈α⊗Component(comp),
␈↓ α␈↓↓Coordinate(coord)
␈↓"β␈↓ α␈↓↓␈↓ αHContents-Appearance(mt-contents, coord, x) ←
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬The appearance of an empty contents at a coordinate is intentionally left unspecified as yet.␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHContents-Appearance(add-component(cont,␈α,comp,␈α,coord'),␈α,coord,␈α,illum)␈α+←
␈↓ α␈↓↓Component-In(comp,␈α&minus(coord,␈α&coord'),␈α%true),␈α&Contents-In(cont,␈α&coord,␈α%true),
␈↓ α␈↓↓Component-Appearance(comp,␈α∃minus(coord,␈α∃coord'),␈α⊗illum1),␈α∃Contents-Appearance(cont,
␈↓ α␈↓↓coord, illum2), Combine(illum1, illum2, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHContents-Appearance(add-component(cont,␈α,comp,␈α,coord'),␈α,coord,␈α,illum)␈α+←
␈↓ α␈↓↓Component-In(comp,␈α%minus(coord,␈α$coord'),␈α%true),␈α$Contents-In(cont,␈α%coord,␈α$false),
␈↓ α␈↓↓Component-Appearance(comp, minus(coord, coord'), illum)
␈↓"β␈↓ α␈↓↓␈↓ αHContents-Appearance(add-component(cont,␈α,comp,␈α,coord'),␈α,coord,␈α,illum)␈α+←
␈↓ α␈↓↓Component-In(comp, minus(coord, coord'), false), Contents-Appearance(cont, coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHContents-In(mt-contents, coord, false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHContents-In(add-component(cont,␈α∂comp,␈α∞coord'),␈α∂coord,␈α∞true)␈α∂←␈α∞Component-In(comp,
␈↓ α␈↓↓minus(coord, coord'), true)
␈↓"β␈↓ α␈↓↓␈↓ αHContents-In(add-component(cont,␈α↔comp,␈α↔coord'),␈α↔coord,␈α↔true)␈α↔←␈α↔Contents-In(cont,
␈↓ α␈↓↓coord, true)
␈↓"β␈↓ α␈↓↓␈↓ αHContents-In(add-component(cont,␈α
comp,␈α∞coord'),␈α
coord,␈α
false)␈α∞←␈α
Component-In(comp,
␈↓ α␈↓↓minus(coord, coord'), false), Contents-In(cont, coord, false)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Contents
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Component ␈↓¬ This type is simply the union of View, Text, and Figure.␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHComponent(make-vcomp(view)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHComponent(make-tcomp(text)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHComponent(make-fcomp(figure)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHComponent-Appearance(make-vcomp(view),␈α∞coord,␈α∞illum)␈α∞←␈α∞View-Appearance(view,
␈↓ α␈↓↓coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHComponent-Appearance(make-tcomp(text),␈α_coord,␈α↔illum)␈α_←␈α↔Text-Appearance(text,
␈↓ α␈↓↓coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHComponent-Appearance(make-fcomp(figure),␈α?␈α8coord,␈α?␈α8illum)␈α?␈α8←
␈↓ α␈↓↓Figure-Appearance(figure, coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHComponent-In(make-vcomp(view), coord, tv) ← View-In(view, coord, tv)
␈↓"β␈↓ α␈↓↓␈↓ αHComponent-In(make-tcomp(text), coord, tv) ← Text-In(text, coord, tv)
␈↓"β␈↓ α␈↓↓␈↓ αHComponent-In(make-fcomp(figure), coord, tv) ← Figure-In(figure, coord, tv)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Component
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE View
␈↓"β␈↓ α␈↓↓␈↓ αHView(mt-view) ←
␈↓"β␈↓ α␈↓↓␈↓ αHView(add-picture(view, coord, picture-id, picture)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHView-Appearance(mt-view, coord, x) ←
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬Again, we leave unspecified the appearance of the mt-view at any coordinate␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHView-Appearance(add-picture(v,␈α≥coord',␈α≥id,␈α≥p),␈α≥coord,␈α≥illum)␈α≥←␈α≥Picture-In(p,
␈↓ α␈↓↓minus(coord, coord'), true), Picture-Appearance(p, minus(coord, coord'), illum)
␈↓"β␈↓ α␈↓↓␈↓ αHView-Appearance(add-picture(v,␈α≥coord',␈α≥id,␈α≥p),␈α≥coord,␈α≥illum)␈α≥←␈α≥Picture-In(p,
␈↓ α␈↓↓minus(coord, coord'), false), View-Appearance(v, coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHView-In(mt-view, coord, false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHView-In(add-picture(v,␈α↔coord',␈α⊗id,␈α↔p),␈α↔coord,␈α⊗true)␈α↔←␈α↔Picture-In(p,␈α⊗minus(coord,
␈↓ α␈↓↓coord'), true)
␈↓"β␈↓ α␈↓↓␈↓ αHView-In(add-picture(v, coord', id, p), coord, true) ← View-In(v, coord, true)
␈↓ α␈↓␈↓ ε␈↓  7␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHView-In(add-picture(v,␈α⊗coord',␈α⊗id,␈α⊗p),␈α∃coord,␈α⊗false)␈α⊗←␈α⊗Picture-In(p,␈α∃minus(coord,
␈↓ α␈↓↓coord'), false), View-In(v, coord, false)
␈↓"β␈↓ α␈↓↓␈↓ αHFindPictures(mt-view, coord, mt-idlist) ←
␈↓"β␈↓ α␈↓↓␈↓ αHFindPictures(add-picture(v,␈α⊂coord',␈α⊂id,␈α∂p),␈α⊂coord,␈α⊂idlist-insert(id,idl))␈α⊂←␈α∂Picture-In(p,
␈↓ α␈↓↓minus(coord, coord'), true), FindPictures(v, coord, idl)
␈↓"β␈↓ α␈↓↓␈↓ αHFindPictures(add-picture(v,␈α∩coord',␈α∩id,␈α∩p),␈α∩coord,␈α∩idl)␈α∩←␈α∩Picture-In(p,␈α∩minus(coord,
␈↓ α␈↓↓coord'), false), FindPictures(v, coord, idl)
␈↓"β␈↓ α␈↓↓␈↓ αHDeletePicture(mt-view, id, mt-view) ←
␈↓"β␈↓ α␈↓↓␈↓ αHDeletePicture(add-picture(v, coord, id, p), id, v) ←
␈↓"β␈↓ α␈↓↓␈↓ αHDeletePicture(add-picture(v,coord,id',p),␈α?␈α	id,␈α?␈α	add-picture(v',coord,id',p))␈α?␈αλ←
␈↓ α␈↓↓PictureId-equal(id, id', false), DeletePicture(v, id, v')
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE View
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Idlist ␈↓¬ Sequence of ␈↓∧PictureId
␈↓"β␈↓ α␈↓↓␈↓ αHIdlist(mt-idlist) ←
␈↓"β␈↓ α␈↓↓␈↓ αHIdlist(idlist-insert(id,idl)) ← PictureId(id), Idlist(idl)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Idlist
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Text
␈↓"β␈↓ α␈↓↓␈↓ αHText(mt-text) ←
␈↓"β␈↓ α␈↓↓␈↓ αHText(text-insert(par, txt)) ← Paragraph(par), Text(txt)
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬ macro: ␈↓∧down(d)␈↓¬ is ␈↓∧minus(coord, times(d, UnitVectorDown)
␈↓"β␈↓ α␈↓↓␈↓ αHText-Appearance(mt-text, coord, x) ←
␈↓"β␈↓ α␈↓↓␈↓ αHText-Appearance(text-insert(par,␈αtxt),␈αcoord,␈αillum)␈α←␈αParagraph-In(par,␈αcoord,␈αtrue),
␈↓ α␈↓↓Paragraph-Appearance(p, coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHText-Appearance(text-insert(par,␈αtxt),␈α
coord,␈αillum)␈α
←␈αParagraph-In(par,␈αcoord,␈α
false),
␈↓ α␈↓↓Paragraph-Height(par, d), Text-Appearance(txt, down(d), illum)
␈↓"β␈↓ α␈↓↓␈↓ αHText-In(mt-text, coord, false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHText-In(text-insert(par, txt), coord, true) ← Paragraph-In(par, coord, true)
␈↓"β␈↓ α␈↓↓␈↓ αHText-In(text-insert(par,␈α⊃txt),␈α⊃coord,␈α⊃true)␈α⊃←␈α⊃Paragraph-Height(par,␈α⊃d),␈α⊃Text-In(txt,
␈↓ α␈↓↓down(d), true)
␈↓"β␈↓ α␈↓↓␈↓ αHText-In(text-insert(par,␈α≡txt),␈α≡coord,␈α≡false)␈α≡←␈α≡Paragraph-In(par,␈α≡coord,␈α≥false),
␈↓ α␈↓↓Paragraph-Height(par, d), Text-In(txt, down(d), false)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Text
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Paragraph ␈↓¬macro: Down(d) is Minus(coord, Times(d, UnitVectorDown) ␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHParagraph(make-paragraph(parlooks, eng-string)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Firstline(make-paragraph(look,␈α2s),␈α1line)␈α2←␈α2Parlooks-width(look,␈α1w),
␈↓ α␈↓↓EngString-Firstline(s, w, line)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Balance(make-paragraph(look,␈α?␈α
s),␈α?␈α
make-paragraph(look,␈α?␈α
s'))␈α?␈α	←
␈↓ α␈↓↓Parlooks-width(look,w) EngString-Balance(s, w)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Null(make-paragraph(look,s), tv) ← String-Null(s,tv)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Space(make-paragraph(look,s), dist) ← ParLooks-space(look, dist)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Height(p,dist) ← Par-Null(p,true), Par-Space(p, dist)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Height(p,␈α)dist1␈α(+␈α)dist2)␈α(←␈α)Par-Null(p,false),␈α)Par-Firstline(p,␈α(line),
␈↓ α␈↓↓Line-Height(line,dist1), Par-Balance(p, p'), Par-Height(p', dist2)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-In(p,␈α
coord,␈αtrue)␈α
←␈αPar-Null(p,␈α
false),␈αPar-Firstline(p,␈α
line),␈α
Par-Space(p,␈αdist1),
␈↓ α␈↓↓Line-Ascent(line, dist2), Line-In(line, Down(dist1 + dist2), true)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-In(p,␈α∞coord,␈α∞true)␈α
←␈α∞Par-Null(p,␈α∞false),␈α
Par-Balance(p,␈α∞p'),␈α∞Par-Firstline(p,␈α
line),
␈↓ α␈↓↓Line-Height(line, dist), Par-In(p', Down(dist), true)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-In(p, coord, false) ← Par-Null(p, true)
␈↓ α␈↓␈↓ β␈↓  8␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHPar-In(p,␈αcoord,␈αfalse)␈α←␈αPar-Null(p,␈αfalse),␈αPar-Firstline(p,␈αline),␈αPar-Space(p,␈αdist1),
␈↓ α␈↓↓Line-Ascent(line,␈α↔dist2),␈α↔Line-In(line,␈α↔Down(dist1␈α↔+␈α↔dist2),␈α↔false),␈α↔Par-Balance(p,␈α⊗p'),
␈↓ α␈↓↓Line-Height(line, dist), Par-In(p', Down(dist), false)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Appearance(p,␈α≤coord,␈α≤illum)␈α≠←␈α≤Par-Firstline(p,␈α≤line),␈α≤Par-Space(p,␈α≠dist1),
␈↓ α␈↓↓Line-Ascent(line,␈α∪dist2),␈α∪Line-In(line,␈α∪Down(dist1␈α∪+␈α∪dist2),␈α∪true),␈α∪Line-Appearance(line,
␈↓ α␈↓↓Down(dist1 + dist2), illum)
␈↓"β␈↓ α␈↓↓␈↓ αHPar-Appearance(p,coord,illum)␈α'←␈α'Par-Firstline(p,␈α'line),␈α'Par-Space(p,␈α&dist1),
␈↓ α␈↓↓Line-Ascent(line,␈α↔dist2),␈α↔Line-In(line,␈α↔Down(dist1␈α↔+␈α↔dist2),␈α↔false),␈α↔Par-Balance(p,␈α⊗p'),
␈↓ α␈↓↓Line-Height(line, dist), Par-Appearance(p', Down(dist), illum)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE PARAGRAPH
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE EnglishString
␈↓"β␈↓ α␈↓↓␈↓ αHEngString(mt-string) ←
␈↓"β␈↓ α␈↓↓␈↓ αHEngString(string-insert(char, string) ← Character(char), EngString(string)
␈↓"β␈↓ α␈↓↓␈↓ αHEngString-Firstline(mt-string, dist, mt-line) ←
␈↓"β␈↓ α␈↓↓␈↓ αHEngString-Firstline(string-insert(c,s), d, c) ← SplitHere(s,c,d,true)
␈↓"β␈↓ α␈↓↓␈↓ αHEngString-Firstline(string-insert(c,s),␈α↔d,␈α_line-insert(c,␈α↔line))␈α_←␈α↔SplitHere(s,c,d,false),
␈↓ α␈↓↓Character-width(c,w), EngString-Firstline(s, d-w, line)
␈↓"β␈↓ α␈↓↓␈↓ αHEngString-Balance(mt-string, d, mt-string)←
␈↓"β␈↓ α␈↓↓␈↓ αHEngString-Balance(string-insert(c,s), d, s) ← SplitHere(s,c,d,true)
␈↓"β␈↓ α␈↓↓␈↓ αHEngString-Balance(string-insert(c,s),␈α?␈α	d,␈α?␈α	str)␈α?␈α	←␈α?␈α	Character-width(c,w),
␈↓ α␈↓↓EngString-Balance(s, d-w, str)
␈↓"β␈↓ α␈↓↓␈↓ αHSplitHere(mt-string, c, d,true) ←
␈↓"β␈↓ α␈↓↓␈↓ αHSplitHere(string-insert(c',s), c, d, true) ← Character-Equal(c', quoteCR, true)
␈↓"β␈↓ α␈↓↓␈↓ αHSplitHere(string-insert(c',s),␈α→c,␈α_d,␈α→true)␈α_←␈α→Character-Equal(c',␈α→quoteSpace,␈α_false),
␈↓ α␈↓↓Character-width(c,w), Character-width(c',w'), LessThan(d, w+w',true)
␈↓"β␈↓ α␈↓↓␈↓ αHSplitHere(string-insert(c',s),␈α∂c,␈α∞d,␈α∂true)␈α∞←␈α∂LexicalBreak(c,␈α∞c',␈α∂true),␈α∞Character-width(c,
␈↓ α␈↓↓w), WordFits(s, c', d-w, false)
␈↓"β␈↓ α␈↓↓␈↓ αHSplitHere(string-insert(c',s),␈α≤c,␈α≤d,␈α≤false)␈α≤←␈α≤Character-Equal(c',␈α≤quoteCR,␈α≠false),
␈↓ α␈↓↓Character-Equal(c',␈α(quoteSpace,␈α(tv1),␈α(Character-width(c,w),␈α'Character-width(c',w'),
␈↓ α␈↓↓LessThan(d,␈α∞w+w',␈α∞tv2),␈α∞Not(tv2,tv2'),␈α∞Or(tv1,␈α∞tv2',␈α∞true),␈α∞LexicalBreak(c,␈α∞c',␈α∞tv3),␈α
Not(tv3,
␈↓ α␈↓↓tv3'), Character-width(c, w), WordFits(s, c', d-w, tv4), Or(tv3', tv4, true)
␈↓"β␈↓ α␈↓↓␈↓ αHNot(true, false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHNot(false, true) ←
␈↓"β␈↓ α␈↓↓␈↓ αHOr(true, tv, true) ←
␈↓"β␈↓ α␈↓↓␈↓ αHOr(tv, true, true) ←
␈↓"β␈↓ α␈↓↓␈↓ αHOr(false, false, false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLexicalBreak(current,␈α~next,␈α~true)␈α→←␈α~Character-Equal(current,␈α~quoteSpace,␈α→true),
␈↓ α␈↓↓Character-Equal(next, quoteSpace, false)
␈↓"β␈↓ α␈↓↓␈↓ αHLexicalBreak(current,␈α∃next,␈α∃true)␈α∀←␈α∃Character-Equal(current,␈α∃quoteHyphen,␈α∀true),
␈↓ α␈↓↓Character-Equal(next,␈α≠quoteHyphen,␈α≠false),␈α≠Character-Equal(next,␈α≤quoteSpace,␈α≠false)
␈↓ α␈↓↓LexicalBreak(current, next, false) ← Character-Equal(next, quoteSpace, true)
␈↓"β␈↓ α␈↓↓␈↓ αHLexicalBreak(current,␈α↔next,␈α_false)␈α↔←␈α↔Character-Equal(current,␈α_quoteSpace,␈α↔false),
␈↓ α␈↓↓Character-Equal(current, quoteHyphen, false)
␈↓"β␈↓ α␈↓↓␈↓ αHLexicalBreak(current,␈α↔next,␈α_false)␈α↔←␈α↔Character-Equal(current,␈α_quoteSpace,␈α↔false),
␈↓ α␈↓↓Character-Equal(next, quoteHyphen, true),
␈↓"β␈↓ α␈↓↓␈↓ αHWordFits(mt-string, c, d, true) ←
␈↓"β␈↓ α␈↓↓␈↓ αHWordFits(string-insert(c',s), c, d, true) ← Character-Equal(c, quoteCR, true)
␈↓"β␈↓ α␈↓↓␈↓ αHWordFits(string-insert(c',s), c, d, true) ← Character-Equal(c, quoteSpace, true)
␈↓ α␈↓␈↓ ∧␈↓  9␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHWordFits(string-insert(c',s),␈α∞c,␈α
d,␈α∞true)␈α
←␈α∞LexicalBreak(c,c',true),␈α
Character-width(c,w),
␈↓ α␈↓↓LessThan(d, w, false)
␈↓"β␈↓ α␈↓↓␈↓ αHWordFits(string-insert(c',s),␈α⊃c,␈α⊃d,␈α∩true)␈α⊃←␈α⊃Character-width(c,␈α∩w),␈α⊃Character-width(c',
␈↓ α␈↓↓w'), LessThan(d, w+w', false), WordFits(s, c', d-w, true)
␈↓"β␈↓ α␈↓↓␈↓ αHWordFits(string-insert(c',s),␈α≥c,␈α≥d,␈α≥false)␈α≥←␈α≥Character-Equal(c,␈α≥quoteCR,␈α≤false),
␈↓ α␈↓↓Character-Equal(c,␈α7quoteSpace,␈α6false),␈α7LexicalBreak(c,c',tv1),␈α7Not(tv1,␈α6tv1'),
␈↓ α␈↓↓Character-width(c,w),␈α∨LessThan(d,␈α∨w,␈α tv2),␈α∨Or(tv1',␈α∨tv2),␈α Character-width(c',␈α∨w'),
␈↓ α␈↓↓LessThan(d, w+w', tv3), WordFits(s, c', d-w, tv4), Not(tv4, tv4'), Or(tv3, tv4', true)
␈↓"β␈↓ α␈↓↓␈↓ αHString-Null(mt-string, true) ←
␈↓"β␈↓ α␈↓↓␈↓ αHString-Null(string-insert(c, s), false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE EnglishString
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE LINE
␈↓"β␈↓ α␈↓↓␈↓ αHLine(mt-line) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLine(line-insert(c, l)) ← Character(c), Line(l)
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬Line-Appearance(mt-line,␈α∂coord,illum)␈α⊂intentionally␈α∂left␈α∂unspecified␈α⊂macro:␈α∂␈↓∧Right(d)␈↓¬␈α∂is␈α⊂␈↓∧Minus(coord,␈α∂Times(d,
␈↓ α␈↓∧UnitVectorRight)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Appearance(line-insert(c,␈α_ln),␈α_coord,␈α→illum)␈α_←␈α_Character-In(c,␈α→coord,␈α_true),
␈↓ α␈↓↓Character-Appearance(c, coord, illum)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Appearance(line-insert(c,␈α↔ln),␈α↔coord,␈α_illum)␈α↔←␈α↔Character-In(c,␈α_coord,␈α↔false),
␈↓ α␈↓↓Character-width(c, w), Line-Appearance(ln, Right(w), illum)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-In(mt-line, coord, false) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLine-In(line-insert(c, ln), coord, true) ← Character-In(c, coord, true)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-In(line-insert(c,␈α∞ln),␈α∞coord,␈α∂true)␈α∞←␈α∞Character-width(c,␈α∞w),␈α∂Line-In(ln,␈α∞Right(w),
␈↓ α␈↓↓true)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Height(ln, d1+d2) ← Line-Ascent(ln,d1), Line-Descent(ln, d2)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Ascent(mt-line, 0) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Ascent(line-insert(c,ln),␈α~d)␈α~←␈α~Character-Ascent(c,␈α~d1),␈α≠Line-Ascent(ln,␈α~d2),
␈↓ α␈↓↓Maximum(d1, d2, d)
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Descent(mt-line, 0) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLine-Descent(line-insert(c,ln),␈α∀d)␈α∀←␈α∀Character-Descent(c,␈α∀d1),␈α∃Line-Descent(ln,␈α∀d2),
␈↓ α␈↓↓Maximum(d1, d2, d)
␈↓"β␈↓ α␈↓↓␈↓ αHMaximum(x, y, x) ← LessThan(x, y, false)
␈↓"β␈↓ α␈↓↓␈↓ αHMaximum(x, y, y) ← LessThan(y, x, false)
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬I have assumed the existence of a LessThan predicate that returns true or false␈↓
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE LINE
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Character
␈↓"β␈↓ α␈↓↓␈↓ αHCharacter(make-char(code,␈α≠fig,␈α≠ascent,␈α~descent,␈α≠width))␈α≠←␈α~CharacterCode(code),
␈↓ α␈↓↓Figure(fig), Distance(ascent), Distance(descent), Distance(width)
␈↓"β␈↓ α␈↓↓␈↓ αHCharacter-width(make-char(code, fig, ascent, descent, width), width) ←
␈↓"β␈↓ α␈↓↓␈↓ αHChar-equal(make-char(code, fig, asc, des, w), make-char(code, fig', asc', des', w')) ←
␈↓"β␈↓ α␈↓↓␈↓ αHCharacter-Ascent(make-char(code, fig, ascent, descent, width), ascent) ←
␈↓"β␈↓ α␈↓↓␈↓ αHCharacter-Descent(make-char(code, fig, ascent, descent, width), descent) ←
␈↓"β␈↓ α␈↓↓␈↓ αHChar-Appearance(make-char(cd,f,a,d,w),␈α
coord,␈α
illum)␈α
←␈α
Figure-Appearance(f,␈α
coord,
␈↓ α␈↓↓illum)
␈↓"β␈↓ α␈↓↓␈↓ αHChar-In(make-char(cd,␈αf,␈αa,␈αd,␈αw),␈αcoord,␈αtrue)␈α←␈αFigure-In(f,␈αcoord,␈αtrue),␈αIncreasing(
␈↓ α␈↓↓a,␈α
project(coord,␈α
unitvectordown),␈α
d,␈α
true),␈α
Increasing(␈α
0,␈α
project(coord,␈α
unitvectorright),␈αw,
␈↓ α␈↓↓true)
␈↓"β␈↓ α␈↓↓␈↓ αHChar-In(make-char(cd, f, a, d, w), coord, false) ← Figure-In(f, coord, false)
␈↓ α␈↓␈↓ 
w␈↓  10␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHChar-In(make-char(cd,␈α⊗f,␈α⊗a,␈α⊗d,␈α⊗w),␈α⊗coord,␈α⊗false)␈α⊗←␈α⊗Increasing(␈α⊗a,␈α∃project(coord,
␈↓ α␈↓↓unitvectordown), d, false)
␈↓"β␈↓ α␈↓↓␈↓ αHChar-In(make-char(cd,␈α⊗f,␈α⊗a,␈α⊗d,␈α⊗w),␈α⊗coord,␈α⊗false)␈α⊗←␈α⊗Increasing(␈α⊗0,␈α∃project(coord,
␈↓ α␈↓↓unitvectorright), w, false)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Character
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Figure
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬Type␈απFigure␈αλwill␈απnecessarily␈απinclude␈αλspecifications␈απof␈αλthe␈απAppearance␈απand␈αλIn␈απpredicates␈αλfor␈απthe␈απtype.␈αλThis␈απtype␈αλis␈απleft
␈↓ α␈↓¬unspecified␈αλas␈αλit␈αλmay␈αλbe␈αλdependent␈απupon␈αλthe␈αλtarget␈αλsystem.␈αλ Clearly,␈αλa␈αλmore␈απflexible␈αλspecification␈αλof␈αλFigure␈αλis␈αλpossible␈αλfor␈απa
␈↓ α␈↓¬bit mapped display than is possible given a character mapped display. ␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Figure
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE␈αλCoordinate␈αλ␈↓¬␈απThis␈αλtype␈αλis␈απnot␈αλyet␈αλspecified.␈απIt␈αλneeds␈αλat␈απleast␈αλthe␈αλfunctions␈απminus,␈αλtimes,␈αλand␈αλproject,␈απand
␈↓ α␈↓¬the␈α	constants␈α	unitvectorright␈α	and␈α	unitvectordown.␈α	 A␈α	2-dimensional␈α
vector␈α	space␈α	would␈α	do,␈α	and␈α	one␈α	might␈α	consider␈α
this␈α	a
␈↓ α␈↓¬primitive type of the system one is using.␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Coordinate
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Distance
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬ Again,␈απthis␈απtype␈απshould␈απbe␈απavailable␈απalready␈απon␈απthe␈απtarget␈απsystem.␈απ One␈απsimply␈απneeds␈απto␈απdefine␈απthe␈απmapping␈απfrom␈απthe
␈↓ α␈↓¬predicate form used in the Horn clauses to the functions available.␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Distance
␈↓"β␈↓ α␈↓↓␈↓ αHTYPE Font
␈↓"β␈↓ α␈↓↓␈↓ αHFont(mt-font) ←
␈↓"β␈↓ α␈↓↓␈↓ αHFont(addcharacter(font, char)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLookup(mt-font, code, x) ← ␈↓¬another unspecified pathological case␈↓∧
␈↓"β␈↓ α␈↓↓␈↓ αHLookup(addcharacter(fnt, make-char(cd, f, a, d, w)), cd, make-char(cd, f, a, d, w)) ←
␈↓"β␈↓ α␈↓↓␈↓ αHLookup(addcharacter(fnt,␈α2make-char(cd,␈α1f,␈α2a,␈α2d,␈α1w)),␈α2code,␈α2c)␈α1←
␈↓ α␈↓↓CharacterCode-Equal(cd, code, false), Lookup(fnt, code, c)
␈↓"β␈↓ α␈↓↓␈↓ αHEND TYPE Font
␈↓"β␈↓ α␈↓↓␈↓ αHPRIMITIVES
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓¬The␈αprimitive␈α
predicates␈αthat␈α
relate␈αthe␈α
logic␈αto␈α
a␈αparticular␈α
system␈αinclude␈α
the␈αtypes␈α
Boundary,␈αTranslation,
␈↓ α␈↓¬Coordinate,␈αIllumination,␈αand␈αthe␈αpredicates,␈αsuch␈αas␈αCompute-Position,␈αLies-In,␈αand␈αMinus,␈αthat␈αoperate␈αon␈αthem.␈αFor
␈↓ α␈↓¬example,␈αan␈αillumination␈α
may␈αbe␈αone␈α
of␈αtwo␈αvalues␈α
(white/black),␈αone␈αof␈α
several␈αshades␈αof␈α
grey,␈αor␈αa␈α
more␈αcomplex
␈↓ α␈↓¬combination of hue and intensity, depending on the capabilities of the system one is designing.
␈↓ α␈↓␈↓ 
|␈↓  11␈↓